T:Type, c:T, i:Id. AtomFree(Type;T)  R-Feasible(constR{x:ut2}(T; c; i)) 

latex

Definitions

Raframe-k(x1), P  Q, t  T, Rbframe-k(x1), (x,yL.P(x;y)), IdDeq, tl(l), R-Feasible(R), b, Rsends-ds(x1), {T}, Rsends?(x1), True, Rbframe-L(x1), Rsends-g(x1), Rplus-left(x1), Rpre?(x1), Rsends-dt(x1), p  q, R-interface-compat(A;B), A & B, Reffect-x(x1), Reffect?(x1), Rsframe?(x1), SQType(T), Reffect-ds(x1), Rrframe-L(x1), false, P & Q, ij, Rsends-l(x1), constR{$x:ut2}(T; c; i), i<j, 2of(t), nth_tl(n;as), Rda(R), Rsframe-tag(x1), Rframe-x(x1), Rplus-right(x1), Rrframe?(x1), if b t else f fi, Reffect-knd(x1), Rsends-T(x1), true, Id, Raframe?(x1), R-base-domain(R), l[i], i=j, xL. P(x), x:A. B(x), Rsframe-L(x1), hd(l), Rbframe?(x1), Rpre-a(x1), Rrframe-x(x1), Top, Reffect-T(x1), A || B, x. t(x), 1of(t), Rframe?(x1), Y, Rds(R), R-frame-compat(A;B), Rsframe-lnk(x1), R-loc(R), Raframe-L(x1), "$x", Prop, Normal(T), ||as||, Atom2Deq, Rsends-knd(x1), a = b, p = q, Rpre-ds(x1), eq_atom$n(x;y), Rplus?(x1), eqof(d), Rframe-L(x1), Rnone?(x1), {i..j}, Dec(P), x(s), (x  l), x:A. B(x), , Unit, , P  Q, P  Q,

Lemmas

R-feasible-Rlist, eqff to assert, assert-eq-id, assert wf, iff transitivity, assert of bnot, Rframe wf, eq id wf, fpf-empty-compatible-right, top wf, bnot wf, fpf-empty wf, Knd wf, Rinit wf, int seg wf, not wf, id-deq wf, not functionality wrt iff, R-Feasible wf, fpf-compatible-self, eqtt to assert, fpf-single wf, es realizer wf, l member wf, Kind-deq wf, decidable int equal, atom-free wf, bool wf, Id wf